26
0 true
1 ( >= basic_right_pic_kid_0_width 0.0 )
2 ( >= basic_right_pic_kid_0_hight 0.0 )
3 ( >= basic_right_pic_kid_1_x 0.0 )
4 ( >= basic_right_pic_kid_1_width 0.0 )
5 ( >= basic_right_pic_kid_1_hight 0.0 )
6 ( <= ( + basic_right_pic_kid_0_width ( * -1.0 basic_right_pic_width ) ) 0.0 )
7 ( <= basic_right_pic_kid_0_x 0.0 )
8 ( >= basic_right_pic_kid_0_x 0.0 )
9 ( <= ( + basic_right_pic_kid_1_width basic_right_pic_kid_1_x ( * -1.0 basic_right_pic_width ) ) 0.0 )
10 ( >= ( + basic_right_pic_kid_1_width basic_right_pic_kid_1_x ( * -1.0 basic_right_pic_width ) ) 0.0 )
11 ( <= basic_right_pic_kid_0_y 0.0 )
12 ( >= basic_right_pic_kid_0_y 0.0 )
13 ( <= basic_right_pic_kid_1_y 0.0 )
14 ( >= basic_right_pic_kid_1_y 0.0 )
15 ( <= ( + basic_right_pic_hight ( * -1.0 basic_right_pic_kid_0_y ) ( * -1.0 basic_right_pic_kid_0_hight ) ) 0.0 )
16 ( >= ( + basic_right_pic_hight ( * -1.0 basic_right_pic_kid_0_y ) ( * -1.0 basic_right_pic_kid_0_hight ) ) 0.0 )
17 ( <= ( + basic_right_pic_kid_1_hight ( * -1.0 basic_right_pic_hight ) basic_right_pic_kid_1_y ) 0.0 )
18 ( >= ( + basic_right_pic_kid_1_hight ( * -1.0 basic_right_pic_hight ) basic_right_pic_kid_1_y ) 0.0 )
19 ( <= ( + basic_right_pic_kid_0_width ( * -1.0 basic_right_pic_kid_1_x ) basic_right_pic_kid_0_x ) 0.0 )
20 ( >= ( + basic_right_pic_kid_0_width ( * -1.0 basic_right_pic_kid_1_x ) basic_right_pic_kid_0_x ) 0.0 )
21 ( <= ( + basic_right_pic_kid_1_width ( * -1.0 basic_right_pic_kid_0_width ) ) 0.0 )
22 ( >= ( + basic_right_pic_kid_1_width ( * -1.0 basic_right_pic_kid_0_width ) ) 0.0 )
23 basic_right_pic_kid_0_feasible
24 basic_right_pic_kid_1_feasible
25 basic_right_pic_feasible
0
25
( 1 )
( 2 )
( 3 )
( 4 )
( 5 )
( 6 )
( 7 )
( 8 )
( 9 )
( 10 )
( 11 )
( 12 )
( 13 )
( 14 )
( 15 )
( 16 )
( 17 )
( 18 )
( 19 )
( 20 )
( 21 )
( 22 )
( 23 )
( 24 )
( 25 )
sat
